A:Type, d1, d2:EqDecider(A), B:(AType), f:a:A fp B(a), x:A, z:B(x). f(x)?z = f(x)?z  B(x) 

latex

Definitions	x:A. B(x), x(s), f(x)?z, if b then t else f fi , f(x), t  T, x. t(x), P  Q, tt, t.2, , ff, a:A fp B(a), x  dom(f), , Unit, P  Q, P & Q, t.1, A, False,
Lemmas	fpf-dom wf, fpf-trivial-subtype-top, bool wf, eqtt to assert, assert-deq-member, l member wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, deq-member wf, fpf wf, deq wf